M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v)  Prop 

latex

Definitions	MsgA, M.state, M.da(a), M.pre(a,s,v), z != f(x)  P(a;z), b, x  dom(f), IdDeq, f(x), P  Q, a:A fp B(a), Prop, Valtype(da;k), f(x)?z, x. t(x), Knd, KindDeq, locl(a), Top, State(ds), x:A. B(x), t  T, Id
Lemmas	Id wf, ma-state wf, top wf, locl wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-valtype wf, fpf-trivial-subtype-top, fpf-ap wf, id-deq wf, fpf-dom wf, assert wf, msga wf